MatchingOnCoinductiveRecord.agda:21,5-10
Pattern matching on coinductive types is not allowed
when checking that the pattern inn y has type U
